DI    	      	180772	DIRECTORY OF 1,JMC
SNOOP 	      	140772	Log of session with NLS at SRI
ADMIND	AX    	      	JMC revision of two axioms by Igarashi
BLIROB	AX    	      	axioms for blind robot problem
BLISET	AX    	      	adding set of objects at location to blirob
COND  	AX    	      	non-Scott axioms for conditional expressions
EQUA  	AX    	      	equality axioms
IGR   	AX    	      	axioms about when predicate admits induction
INT   	AX    	      	integer axioms with SUCC and PRED as functions
LISP  	AX    	      	lisp axioms
LIST  	AX    	      	axioms for lists of individuals
ORD1  	AX    	      	≤ as a predicate
ORD2  	AX    	      	orderings as individuals
REST  	AX    	180772	Restrictions of maps and such like.
SCINT 	AX    	JMC   	Axioms for integers with the functions as individuals.
SCOTT 	AX    	      	Scott orderings
SCWORL	AX    	140772	Axioms for terms in "Scott worlds"
SET   	AX    	      	set axioms
TERMS 	AX    	12772 	Axioms for terms
W0    	AX    	140772	Scott world W0 contains integer and LISP terms
ADD   	COM   	      	17+34=51
BLIROB	COM   	JMC   	commands for a partial proof of blirob.
BLISET	COM   	JMC   	commands for proof that SIT(Z) is unchanged by moving.
TH1   	COM   	JMC   	COMMANDS FOR PROOF THAT M'+N=(M+N)'.
CKSUM 	DAT   	180772	CHECKSUMS OF FILES
BLIROB	DOC   	      	Explanation of blind robot problem
IMPROV	DOC   	      	old request for improvements to PCHECK
NEWRUL	DOC   	JMC   	documentation of elementary lisp assertion rules
SETRUL	DOC   	      	proposed rules for asserting set membership,etc
SORTS 	DOC   	      	proposal for concealed sorting in PCHECK
TRANS 	DOC   	JMC   	how to translate rlisp files to lisp.
SYSTEM	HAC   	JMC   	how to print messages,get characters on imlac,
PCHECK	M1    	JMC   	mods to pcheck to allow elementary lisp assertions.
PCHECK	M2    	JMC   	mods to pcheck for quoting and unquoting integers.
IGR   	MSG   	      	from Igarashi about new axioms
WD    	MSG   	      	How to use alphabetic bound variable change
ADD   	PRF   	      	17+34=51
BLISET	PRF   	      	objects sitting at Y are unchanged by moving
COND  	PRF   	      	(p→(p→a,b),c)=(p→a,c)
FALSE 	PRF   	180772	Russell's paradox
TH1   	PRF   	      	m'+n=(m+n)'
PUZZ  	RLS   	      	Knuth's memorial day race
PUZB  	SAI   	JMC   	working version of Knuth's race.
PUZZ  	SAI   	JMC   	non-working version of Knuth's memorial day race.
OPTION	TXT   	180772	System options on login and logout.